$\forall$$T$:Type, $L$:($T$ List). ($\neg$($\uparrow$null($L$))) $\Rightarrow$ (last($L$) $\in$ $T$)